(declare-fun x () (_ BitVec 8))
(declare-fun y () (_ BitVec 8))
(declare-fun r () (_ BitVec 8))
(assert (= r (bvmul x y)))
(assert (= x #x03))
(assert (= y #x07))
(assert (not (= r #x15)))
(assert (not (= r #x00)))
(check-sat)
